Informally speaking, a choreography may be viewed as a contract among multiple cooperations, i.e., a specification of requirements (which may not be executable). An orchestration is the composition of concrete services provided by each cooperation which realizes the contract. The distinction between choreography and orchestration resembles the well studied distinction between sequence diagrams (which describes inter-object system interactions) and state machines (which may be used to describe intra-object state transitions). Likewise, there are two important issues to be solved. If both the choreography and orchestration are given, it is important to guarantee that the two views are consistent, by showing that the orchestration (i.e., implementation) conforms to the choreography (i.e., specification). Given only a choreography, it is necessary to check whether it is implementable and synthesize a prototype implementation (if possible). Web Service Module offers practical solution to both issues, which is self-containing environment for analyzing Web Services (abstractions). The user interface of Web Service Module supports user-friendly editing, simulating and verifying of Web Services. In particular, conformance is verified by showing weak simulation relationship using an on-the-fly model checking algorithm. A scalable lightweight approach is used to solve the synthesis problem.

Figure above shows the workflow of Web Service Module. Given a choreography or an orchestration, a preprocessing component is used to extract relevant information and build a simplified model, in intermediate languages which are designed to capture behaviors of choreography and orchestration. The reason for supporting intermediate languages is twofold. Firstly, heavy languages like WS-CDL or WS-BPEL are designed for machine consumption and therefore are lengthy and complicated in structure. Our intermediate languages focus on the interactive behavioral aspect. Both languages (for choreography and orchestration) have their own parser, compiler as well as formal operational semantics. Therefore, users can quickly write a Web Service model and analyze it using our visualized simulator, verifier and synthesizer. The languages are developed based on previous works of formal models for WS-CDL and WS-BPEL (See next section for details). They cover all main features like synchronous/asynchronous message passing, channel passing, process forking, parallel composition, shared variables, etc. Secondly, Web Service languages are evolving rapidly. Being based an intermediate language gives us opportunity to quickly cope with new syntaxes or features (by tuning the preprocessing component).

Given a choreography, Web Service Module can statically analyze whether it is well-formed, for instance whether it can be implemented in a distributed setting without introducing unexpected behaviors. If the choreography is not implementable, Web Service Module generates an implementable one, by injecting extra message passing into the choreography. Otherwise, Web Service Module may be used to automatically generate a prototype orchestration (which may later be refined and translated to a WS-BPEL document). If an orchestration is provided, the conformance checker allows users to verify whether the orchestration is valid with respect to the choreography.

Currently Web Service Module is still in beta stage. We are actively developing it now. Any suggestion or feedback is extremely welcome.